正規様相論理のための Curry-Howard 対応
本論文では,直観主義様相論理 IKに Curry-Howard 対応する名前呼び及び値呼びの計算系を提案する.名前呼び計算は,圏論的意味論に基づいており,単純型付き名前呼び λ-計算の拡張となっている.本論文は,名前呼び計算の簡約系が強正規化可能性及び合流性を持つことを証明する.また,値呼び計算は,値呼びの λ-計算として定評のある λc-計算の拡張として定義される.名前呼びの場合と同様,値呼び計算に対しても簡約系を与え,その強正規化可能性及び合流性を証明する.加えて,本論文では,値呼び計算の部分体系が名前呼び計算への CPS 変換によって特徴付けられることを示す.最後に,様相論理 IS4への計算系の拡張についても考察する
動機